fpf{-}normalize(${\it eq}$;$g$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$reduce($\lambda$$x$,$f$. $x$ : ($g$.2)($x$) $\oplus$ $f$;$\otimes$;$g$.1)